Nuprl Definition : atom-free-decl
0,22
postcript
pdf
AtomFree(
d
) ==
x
dom(
d
).
A
=
d
(
x
)
AtomFree(Type;
A
)
latex
clarification:
atom-free-decl{i:l}(
T
;
eq
;
d
) == fpf-all(
T
;
eq
;
d
;
x
,
A
.AtomFree(Type{i};
A
))
latex
Definitions
x
dom(
f
).
v
=
f
(
x
)
P
(
x
;
v
)
,
AtomFree(
T
;
x
)
,
Type
FDL editor aliases
atom-free-decl
origin
x
dom(d). A=d(x) 
AtomFree(Type;A)
xdom(d). A=d(x) AtomFree(Type;A)
xdom(f). v=f(x) P(x;v)